COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	color[s86,jmc]		Letter to Mathematical Intelligencer
C00006 ENDMK
C⊗;
color[s86,jmc]		Letter to Mathematical Intelligencer

	Making the proof of the four color theorem more elegant,
intelligible and convincing requires more use of the computer --- not
less.

	The goal should be a single run of a computer program, about which
it has been proved that if the program says yes, the theorem is true.
Developments in computer science may have made this feasible now, and it
will certainly become feasible in the future.


  The proof that
the program is correct in the above sense can itself be checked
by a proof-checking program for the appropriate logical system  ---
for example, set theory axiomatized in first order logic.  The
proof-checking program itself may be proved to correspond to the
logic and this proof may be checked by computer.

	We shall discuss these points in order.

	1. The Appel and Haken proof as explained in this magazine [1]
involves finding an unavoidable set of reducible configurations.
It must be proved that the set is unavoidable and all the configurations
in it are reducible.  Proving reducibility is done for each configuration
by a suitable computer program.  Writing a brute force program that can
be proved correct by current program proving techniques shouldn't be
too difficult, but the actual program used is doubtless elaborated
in order to make it run fast enough.
Several authors have proposed program transformation techniques
that preserve the semantics of a computer program.  The goal should
be to obtain a fast enough program from the readily verified brute
force program by a provably semantics-preserving transformation.

	The same considerations apply to the proof that the set
of configurations is unavoidable.  Of course, nothing need be
proved about any programs or manual techniques for generating
the set of configurations, although understanding may be increased
by providing such proofs.

References: